\begin{tabbing}
ecl{-}es{-}act(${\it es}$;$m$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=ecl\_ind($x$;$k$,${\it test}$.$\lambda$$e_{1}$,$e_{2}$. False;$a$,$b$,${\it aa}$,${\it ab}$.$\lambda$$e_{1}$,$e_{2}$. ${\it aa}$($e_{1}$,$e_{2}$)\+
\\[0ex]$\vee$ $\exists$$e$$\in$($e_{1}$,$e_{2}$].ecl{-}es{-}halt(${\it es}$;$a$)(0,$e_{1}$,pred($e$)) \& ${\it ab}$($e$,$e_{2}$);$a$,$b$,${\it aa}$,${\it ab}$.$\lambda$$e_{1}$,$e_{2}$. ${\it aa}$($e_{1}$,$e_{2}$)
\\[0ex]\& $\forall$$n$$\in$ecl{-}ex($b$).$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$ecl{-}es{-}halt(${\it es}$;$b$)($n$,$e_{1}$,$e$)
\\[0ex]$\vee$ ${\it ab}$($e_{1}$,$e_{2}$) \& $\forall$$n$$\in$ecl{-}ex($a$).$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$ecl{-}es{-}halt(${\it es}$;$a$)($n$,$e_{1}$,$e$);$a$,$b$,${\it aa}$,${\it ab}$.$\lambda$$e_{1}$,$e_{2}$.
\\[0ex]${\it aa}$($e_{1}$,$e_{2}$) \& $\forall$$n$$\in$0.ecl{-}ex($b$).$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$ecl{-}es{-}halt(${\it es}$;$b$)($n$,$e_{1}$,$e$)
\\[0ex]$\vee$ ${\it ab}$($e_{1}$,$e_{2}$) \& $\forall$$n$$\in$0.ecl{-}ex($a$).$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$ecl{-}es{-}halt(${\it es}$;$a$)($n$,$e_{1}$,$e$);$a$,${\it aa}$.$\lambda$$e_{1}$,$e_{2}$.
\\[0ex][$e_{1}$;$e_{2}$]$\sim$([$x$,$y$].\=ecl{-}es{-}halt(${\it es}$;$a$)\+
\\[0ex](0
\\[0ex],$x$
\\[0ex],$y$))$\ast$[$x$,$y$].\=${\it aa}$\+
\\[0ex]($x$
\\[0ex],$y$);$a$,$n$,${\it aa}$.\=if $m$=$_{2}$$n$$\rightarrow$ ecl{-}es{-}halt(${\it es}$;$a$)(0)\+
\\[0ex]else ${\it aa}$ fi;$a$,$n$,${\it aa}$.${\it aa}$;$a$,$l$,${\it aa}$.${\it aa}$)
\-\-\-\-
\end{tabbing}